(set-option :model_validate true)
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(assert (> c 0))
(assert (= (+ c a) 3))
(check-sat)
(assert (= (* b a) 1))
(check-sat)
(reset)
(set-logic QF_BV)
(set-option :model_validate true)
(declare-const v1 Bool)
(declare-const v3 Bool)
(assert (or v1 v3))
(check-sat)
(check-sat)
(reset)
(set-logic QF_BV)
(set-option :model_validate true)
(set-option :model true)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(assert (xor v4 (= v0 v5 v4 v1 v5 v5) v5 v5 v2))
(check-sat)
(check-sat)
(reset)
(set-logic QF_NRA)
(set-option :model_validate true)
(declare-const v1 Bool)
(declare-const v3 Bool)
(declare-const r0 Real)
(declare-const r1 Real)
(assert (or v3 v1))
(check-sat)
(assert (= true true true (distinct 0.0 558186.674 r0 (* r0 25269393063.0 r1 558186.674 558186.674)) true true v1 true true true))
(check-sat)
(reset)
(set-option :model_validate true)
(set-logic QF_NRA)
(declare-fun _substvar_75_ () Bool)
(declare-fun _substvar_89_ () Real)
(set-option :model_validate true)
(declare-const v3 Bool)
(declare-const v15 Bool)
(declare-const r2 Real)
(declare-const r3 Real)
(assert (xor true true false _substvar_75_ v3 false true v15 false (<= 0.756 r2 (* 42.482826 r2 _substvar_89_ r3) 0.0) v3))
(check-sat)
(assert (=> v15 false))
(check-sat)
(reset)
(set-option :model_validate true)
(declare-const v7 Bool)
(declare-const v10 Bool)
(declare-const r4 Real)
(assert (xor v7 true v10 (= (/ 904745.0 r4) 48305217199.0 r4 0.0) true v7))
(check-sat)
(assert (not v7))
(check-sat)
(reset)
(set-option :model_validate true)
(declare-const r2 Real)
(declare-const r5 Real)
(declare-const r8 Real)
(push 1)
(declare-const r28 Real)
(assert (or (>= 97.0 (/ r5 r2) 59.0 0.0 r2) (distinct 3.746 r5 r28 0.0 (/ 0.0 r8))))
(check-sat)
(check-sat)
(assert (<= r2 97.0 r5))
(check-sat)
(reset)
(set-option :model_validate true)
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(assert (> c 0))
(assert (= (+ c a) 3))
(check-sat)
(assert (= (* b a) 1))
(check-sat)
(reset)
(set-logic QF_BV)
(declare-fun _substvar_18_ () Bool)
(set-option :model_validate true)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v4 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v9 Bool)
(declare-const v13 Bool)
(declare-const v14 Bool)
(declare-const v15 Bool)
(declare-const v16 Bool)
(declare-const v17 Bool)
(assert v2)
(push 1)
(push 1)
(push 1)
(declare-const v19 Bool)
(declare-const v20 Bool)
(declare-const v21 Bool)
(declare-const v24 Bool)
(push 1)
(pop 1)
(assert v19)
(assert (= v24 _substvar_18_ v21 v1 (xor v20 v2 (xor v15 v15 v13 v7 v16 v7 v6 v4 v14 v2 v13) v19) true))
(check-sat)
(pop 1)
(pop 1)
(declare-const v31 Bool)
(assert v14)
(assert (= v31 (not v9) v7 v15 (=> v6 v15) (xor v15 v15 v13 v7 v16 v7 v6 v4 v14 v2 v13)))
(push 1)
(assert v6)
(assert v17)
(check-sat)
(reset)
(set-logic QF_BV)
(set-option :model_validate true)
(declare-const v5 Bool)
(declare-const v8 Bool)
(declare-const v10 Bool)
(declare-const v11 Bool)
(declare-const v17 Bool)
(assert v5)
(push 1)
(assert false)
(check-sat)
(assert v10)
(check-sat)
(pop 1)
(assert (xor (and v5 v10) v17 v8 v11))
(push 1)
(check-sat)
(reset)